\begin{tabbing}
es{-}send{-}atom{-}to(${\it es}$;$e$;$a$;$i$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\exists$${\it e'}$:es{-}E(${\it es}$).\+
\\[0ex]es{-}loc(${\it es}$; ${\it e'}$) $=$ $i$ $\in$ Id \& es{-}rcv{-}atom(${\it es}$;${\it e'}$;$a$) \& es{-}sender(${\it es}$; ${\it e'}$) $=$ $e$ $\in$ es{-}E(${\it es}$)
\-
\end{tabbing}